package no.uio.ifi.cop.start;

import java.io.File;
import java.io.IOException;

import java.util.Comparator;
import java.util.Map;

import no.uio.ifi.cop.common.Common;
import no.uio.ifi.cop.common.Log;
import no.uio.ifi.cop.common.AnsiColor;
import no.uio.ifi.cop.util.TimedRunner;
import no.uio.ifi.cop.common.Global;
import no.uio.ifi.cop.parse.option.GetOpt;
import no.uio.ifi.cop.prover.Prover;
import no.uio.ifi.cop.prover.RuleFinder;
import no.uio.ifi.cop.prover.RuleMatcher;
import no.uio.ifi.cop.prover.cmp.InputOrder;
import no.uio.ifi.cop.prover.cmp.NoOfTimes;
import no.uio.ifi.cop.prover.cmp.ReverseOrder;
import no.uio.ifi.cop.prover.cmp.ExistPreference;
import no.uio.ifi.cop.prover.cmp.DynamicNatural;
import no.uio.ifi.cop.prover.cmp.ReverseDynNatural;
import no.uio.ifi.cop.prover.cmp.RandomOrder;
import no.uio.ifi.cop.prover.simple.SimpleRuleFinder;
import no.uio.ifi.cop.prover.rete.ReteRuleFinder;
import no.uio.ifi.cop.prover.hrete.HReteRuleFinder;

/**
 * This is where it all starts.
 *
 * Parse configuration files and input parameters, and start
 * the program.
 *
 *
 * @version 1.0
 * @author  bjarneh@ifi.uio.no
 */


public class Main{

    GetOpt getopt;

    String[] strOpts = {"-timeout",
                        "-loglevel",
                        "-logfile",
                        "-cmp",
                        "-dotfile",
                        "-dotheader",
                        "-dotmax",
                        "-strategy",
                        "-seed",
                        "-order",
                        "-dotfmt",
                        "-maxpaths"};

    String[] boolOpts = {"-help",
                         "-recursive",
                         "-plain",
                         "-paths",
                         "-ignore",
                         "-version",
                         "-single",
                         "-accurate",
                         "-list",
                         "-listcmp",
                         "-verbose",
                         "-hidden"};

    private Main(){}

    public static void main(String[] args){

        Main m = new Main();
        m.init();
        m.go(args);
        Log.close();

    }

    private void init(){

        getopt = new GetOpt();
        getopt.addStringOption("-t -t= -timeout --timeout -timeout= --timeout=");
        getopt.addStringOption("-ll --ll --ll= -ll= -loglevel --loglevel -loglevel= --loglevel=");
        getopt.addStringOption("-lf --lf --lf= -lf= -logfile --logfile --logfile= -logfile=");
        getopt.addStringOption("-c -c= --cmp= -cmp= --cmp -cmp");
        getopt.addStringOption("-d -d= -dot= --dot= -dot --dot -dotfile -dotfile= --dotfile --dotfile=");
        getopt.addStringOption("-dotheader --dotheader -dotheader= --dotheader=");
        getopt.addStringOption("-dotmax -dotmax= --dotmax --dotmax=");
        getopt.addStringOption("-s -s= -strategy --strategy -strategy= --strategy=");
        getopt.addStringOption("-seed --seed -seed= --seed=");
        getopt.addStringOption("-dotfmt --dotfmt -dotfmt= --dotfmt=");
        getopt.addStringOption("-m -m= -maxpaths --maxpaths -maxpaths= --maxpaths=");
        getopt.addStringOption("-o -o= -order -order= --order --order=");
        getopt.addBoolOption("-h -help --help help");
        getopt.addBoolOption("-r -recursive --recursive");
        getopt.addBoolOption("-i -ignore --ignore");
        getopt.addBoolOption("-p -plain --plain");
        getopt.addBoolOption("-P -paths --paths");
        getopt.addBoolOption("-v -version --version");
        getopt.addBoolOption("-single --single");
        getopt.addBoolOption("-l -list --list");
        getopt.addBoolOption("-listcmp --listcmp --listcmp -listcmp");
        getopt.addBoolOption("-V -verbose --verbose");
        getopt.addBoolOption("-hidden --hidden");
        getopt.addBoolOption("-a -accurate --accurate");

    }


    private void go(String[] args){

        // load config file first
        String[] rcArgv = rc2argv();
        // ignore remaining when parsing RC file
        if(rcArgv != null){
            parseArgv(rcArgv);
        }
        // command line overwrites options from config file
        String[] remaining = parseArgv(args);

        if(getopt.isSet("-help")){
            printHelp();
        }else if(getopt.isSet("-version")){
            printVersion();
        }else if(getopt.isSet("-listcmp")){
            listCmp();
        }else if(getopt.isSet("-list")){
            listProperties();
        }

        configureLog();

        if( Global.getBool("-recursive") ){

            for(String s : remaining){
                pathWalkProve(s);
            }

        }else{

            for( String s: remaining ){
                dispatch( s );
            }

        }
    }

    private void proveFileName(String filename){

        Prover prover = new Prover(Global.getBool("storetree"));
        prover.addTheoryFileName(filename);

        String strategy = Global.get("-strategy").toLowerCase();
        String comparator = Global.get("-cmp").toLowerCase();

        Comparator<? super RuleMatcher> cmp = null;

        if( comparator.equals("rev") || comparator.equals("reverse") ){
            cmp = new ReverseOrder();
        } else if( comparator.equals("exist") ){
            cmp = new ExistPreference();
        } else if( comparator.equals("inputorder") || comparator.equals("input") ){
            cmp = new InputOrder();
        } else if( comparator.equals("rnd") || comparator.equals("random") ){
            cmp = new RandomOrder( Global.getLong("-seed") );
        } else if( comparator.equals("drnd") || comparator.equals("drandom") ){
            cmp = new RandomOrder( Global.getLong("-seed") );
            Global.set("dynamic", "true");
        } else if( comparator.equals("dyn") || comparator.equals("dynamic") ){
            cmp = new DynamicNatural();
            Global.set("dynamic", "true");
        } else if( comparator.equals("num") || comparator.equals("number") ){
            cmp = new NoOfTimes();
            Global.set("dynamic", "true");
        } else if( comparator.equals("rdyn") || comparator.equals("rdynamic") ){
            cmp = new ReverseDynNatural();
            Global.set("dynamic", "true");
        }

        boolean dynamic = Global.getBool("dynamic");

        if( strategy.equals("simple") ){
            prover.addRuleFinder( new SimpleRuleFinder( cmp, dynamic ) );
        }else if( strategy.equals("rete") ){
            prover.addRuleFinder( new ReteRuleFinder( cmp, dynamic ) );
        }else if( strategy.equals("hrete") ){
            if( cmp != null ){
                Log.warning(" comparator does not work for 'hrete'");
            }
            prover.addRuleFinder( new HReteRuleFinder() ); 
        }else{
            Log.fatal("%s != [simple, rete, hrete] ", strategy);
        }
        
        // color based on success or failure
        String OK = "ok", NO = "no";
        if( colorize() ){
            OK = String.format("%sok%s", AnsiColor.GREEN, AnsiColor.NORMAL);
            NO = String.format("%sno%s", AnsiColor.RED, AnsiColor.NORMAL);
        }

        if( Global.getBool("-accurate") ) {
            long t0,t1;
            t0 = System.currentTimeMillis();
            prover.run();
            t1 = System.currentTimeMillis();
            double tot = (double) (t1 - t0)/1000L;
            System.out.printf(" %s : %.3f : %s \n", prover.isValid()? OK : NO,
                    tot,
                    createLabel(filename));

        }else{
            long timeout = (long) (Global.getDouble("-timeout") * 1000);
            TimedRunner trunner = new TimedRunner( prover, timeout );

            trunner.run();

            System.out.printf(" %s : %s : %s \n", prover.isValid()? OK : NO,
                    trunner.getFormattetUserTime(),
                    createLabel(filename));
        }

        try{
            if(  prover.graphStored() ){
                String dotstr;
                String header = createHeader(filename);
                if( Global.get("-dotmax").equals("") ){
                    dotstr = prover.getDotGraph(header);
                }else{
                    dotstr = prover.getDotGraph(header, Global.getInt("-dotmax") );
                }

                String dotfile = Global.get("-dotfile").toLowerCase();

                if( dotfile.equals("stdout") || dotfile.equals("system.out") || dotfile.equals("-") ){
                    System.out.printf("%s", dotstr);
                }else if( dotfile.equals("stderr") || dotfile.equals("system.err")){
                    System.err.printf("%s", dotstr);
                }else{
                    Common.spit( Global.get("-dotfile"), dotstr);
                    try{
                        forkGraphviz();
                    }catch(Exception iox){
                        Log.error("%s", iox);
                    }
                }
            }
        }catch(IOException iox){
            Log.fatal("%s", iox);
        }finally{
            // dumpster
            System.gc();
        }

    }

    private void forkGraphviz() throws Exception{
        String dotpath = Common.which("dot");
        if( dotpath != null && !Global.get("-dotfmt").equals("null") ){
            File file = new File(Global.get("-dotfile"));
            if( file.exists() && file.isFile() && file.canRead() ){
                Runtime runtime = Runtime.getRuntime();
                int i = 0;
                String[] cmd = new String[6];
                cmd[i++] = dotpath;
                cmd[i++] = "-T";
                cmd[i++] = Global.get("-dotfmt");
                cmd[i++] = "-o";
                cmd[i++] = file.getName() + "." + Global.get("-dotfmt");
                cmd[i++] = file.getName();

                Process p = Runtime.getRuntime().exec(cmd);
                int ret = p.waitFor();
                if( ret != 0 ){
                    Log.error("dot dit not complete successfully: %d", ret);
                    System.exit(ret);
                }
            }
        }
    }

    private boolean colorize(){
        if(Global.getBool("-plain") ||
           Global.get("os.name").toLowerCase().contains("windows")){
            return false;
        }
        return true;
    }

    private String createHeader(String filename){
        return String.format("  graph [label=\"%s %s %s\", fontsize=%d];\n", 
                              createLabel(filename), 
                              "-dotheader",
                              Global.get("-dotheader"),
                              Global.getInt("-dotheader"));
    }

    private String createLabel(String filename){

        boolean isRandom = false;

        StringBuilder sb = new StringBuilder();
        sb.append(new File(filename).getName());

        sb.append(" -strategy ");
        sb.append(Global.get("-strategy"));

        if( Global.getBool("-ignore") ){
            sb.append(" -ignore");
        }

        sb.append(" -order ");
        sb.append(Global.get("-order"));
        if( Global.get("-order").equals("random") ){
            isRandom = true;
        }

        if( Global.getBool("-single") ){
            sb.append(" -single");
        }

        if( ! Global.get("-strategy").equals("hrete") ){
            String comparator = Global.get("-cmp");
            sb.append(" -cmp ");
            sb.append(comparator);
            if( comparator.equals("rnd")  || comparator.equals("random") ||
                comparator.equals("drnd") || comparator.equals("drandom"))
            {
                isRandom = true;
            }
        }

        if(isRandom){
            sb.append(" -seed ");
            sb.append(Global.get("-seed"));
        }

        return sb.toString();
    }

    private void pathWalkProve(String path){

        String sep = Global.get("file.separator");
        File tmpFile;
        String tmpString;
        File file = new File(path);
        boolean okHidden = false;
        boolean isHidden = false;

        if(! file.exists() ){
            Log.error(" %s: no such file or directory\n", path);
            return;
        }

        if(! file.isDirectory() ){
            Log.warning(" '%s' is not a directory (ignoring, see: -recursive)", path);
        }else{

            okHidden = Global.getBool("-hidden");

            if( file.canRead() ){
                String[] ls = file.list();
                for(String f : ls){
                    tmpString = String.format("%s%s%s",path,sep,f);
                    tmpFile   = new File(tmpString);
                    isHidden  = f.startsWith(".");
                    if( ! isHidden || okHidden ){
                        if( tmpFile.isDirectory() ){
                            pathWalkProve(tmpString);
                        }else{
                            dispatch(tmpString);
                        }
                    }
                }

            }else{
                Log.error("you don't have read access to:%s\n",path);
                return;
            }
        }
    }

    private void dispatch(String filename){

        boolean isAll = false;
        String storeStrat, storeCmp, start, stop;

        storeStrat = Global.get("-strategy");
        storeCmp   = Global.get("-cmp");

        start = ""; stop = "";
        if( colorize() ){
            start = AnsiColor.parse("yellow+bold");
            stop  = AnsiColor.NORMAL;
        }

        if( storeStrat.equals("all") || storeStrat.equals("main") ) {

            System.out.printf("[ Trying %s strategies on: %s%s%s ]\n",
                              storeStrat, start, filename, stop);

            Global.set("storetree", "false");

            if( storeStrat.equals("all") || storeCmp.equals("all") ) {
                isAll = true;
            }
            for( String s : new String[]{"hrete","simple","rete"} ) {

                Global.set("-strategy", s);

                if( isAll ){
                    for( String cmp: comparators() ){

                        Global.set("-cmp", cmp);

                        for(String order : orderings()){

                            Global.set("-order", order);

                            // toggle single
                            Global.set("-single", "false");
                            proveFileName( filename );
                            Global.set("-single", "true");
                            proveFileName( filename );

                        }
                    }
                }else{
                    proveFileName(filename);
                }
            }
        }else if( storeCmp.equals("all") || storeCmp.equals("main") ){

            System.out.printf("[ Trying %s strategy on: %s%s%s ]\n",
                              storeStrat, start, filename, stop);

            Global.set("storetree", "false");

            if( storeCmp.equals("all") ){ isAll = true; }
            for( String cmp: comparators() ){

                Global.set("-cmp", cmp);

                if( isAll ){
                    for(String order : orderings()){

                        Global.set("-order", order);
                        // toggle single
                        Global.set("-single", "false");
                        proveFileName( filename );
                        Global.set("-single", "true");
                        proveFileName( filename );
                    }
                }else{
                    proveFileName( filename );
                }
            }
        }else{
            proveFileName( filename );
        }

        Global.set("-strategy", storeStrat);
        Global.set("-cmp", storeCmp);

    }

    private String[] orderings() {
        return new String[]{"hash","time","random"};
    }

    private String[] comparators() {

        String[] cmps   = {"natural",
                           "reverse",
                           "dynamic",
                           "rdynamic",
                           "numeric",
                           "random",
                           "drandom",
                           "exist",
                           "inputorder"};
        
        if( Global.get("-strategy").equals("hrete") ){
            return new String[]{ "natural" };
        }

        return cmps;
    }


    private String[] rc2argv(){

        String configFile = Global.get("coprc");
        File file = new File( configFile );

        if( ! file.isFile() || ! file.canRead() ){
            return null;
        }

        try{
            String content = Common.slurp( configFile );
            String cleanContent = Common.stripComment('#', content);
            return cleanContent.split("\\s+");
        }catch(IOException iox){
            Log.fatal("%s", iox);
        }

        return null;
    }

    private String[] parseArgv(String[] argv){

        getopt.clear(); // we use this getopt twice

        String[] remaining = getopt.parse(argv);

        for(String option : boolOpts){
            if(getopt.isSet(option)){
                Global.set(option, "true");
            }
        }

        for(String option : strOpts){
            if(getopt.isSet(option)){
                Global.set(option, getopt.getValue(option));
            }
        }

        if(getopt.isSet("-dotfile")){
            Global.set("storetree", "true");
        }

        if(Global.getBool("-verbose")){
            Global.set("-loglevel", "INFO");
        }

        return remaining;
    }

    private void configureLog(){

        String level = Global.get("-loglevel").toUpperCase();

        if( level.equals("DEBUG") ){
            Log.setLevel(Log.DEBUG);
        }else if( level.equals("INFO") ){
            Log.setLevel(Log.INFO);
        }else if( level.equals("WARNING") ){
            Log.setLevel(Log.WARNING);
        }else if( level.equals("ERROR") ){
            Log.setLevel(Log.ERROR);
        }else if( level.equals("FATAL") ){
            Log.setLevel(Log.FATAL);
        }else{
            StringBuilder sb = new StringBuilder();
            sb.append("wrong loglevel: %s\nmust be one of: ");
            sb.append("DEBUG,INFO,WARNING,ERROR,FATAL");
            Log.fatal(sb.toString(), level);
        }

        String logfile = Global.get("-logfile");
        if( ! logfile.equals("") ){
            try{
                Log.add(logfile);
            }catch(Exception x){
                Log.fatal(" %s\n",x);
            }
        }
    }

    private void listCmp(){
        StringBuilder sb = new StringBuilder();
        sb.append("[comparators]\n\n");
        sb.append(" nat/natural     : order rules by preference given below\n");
        sb.append("                   GOAL>PLAIN>DISJUNCT>EXIST>EXISTDISJUNCT\n");
        sb.append("                   if equal preference -> order by input file\n\n");
        sb.append(" rev/reverse     : same as natural, unless equal preference \n");
        sb.append("                   when we use reversed order of input file\n\n");
        sb.append(" dyn/dynamic     : same as natural, unless equal preference \n");
        sb.append("                   when rule least used is preferred\n\n");
        sb.append(" rdyn/rdynamic   : same as natural, unless equal preference \n");
        sb.append("                   when rule with most applications is preferred\n\n");
        sb.append(" num/numeric     : prefer GOAL or least used rule\n\n");
        sb.append(" rnd/random      : prefer GOAL or else random preference\n\n");
        sb.append(" drnd/drandom    : prefer GOAL or else dynamic random preference\n\n");
        sb.append(" exist           : order rules by preference given below\n");
        sb.append("                   GOAL>PLAIN>EXIST>DISJUNCT>EXISTDISJUNCT\n");
        sb.append("                   if equal preference -> order by input file\n\n");
        sb.append(" input/inputorder: order by input file\n\n");
        sb.append(" main            : all of the above\n\n");
        sb.append(" all             : main comparators with different types or ordering\n");
        System.out.printf("\n%s\n", sb.toString());
        System.exit(0);
    }

    private void listProperties(){
        Global.list(System.out);
        System.exit(0);
    }

    private void printHelp(){

        StringBuilder sb = new StringBuilder();
        sb.append("\ncop - Coherent Theorem Prover\n\n");
        sb.append("usage: cop [OPTIONS] input.gl\n\n");
        sb.append("Options:\n\n");
        sb.append(" -h --help      :  print this message and exit\n");
        sb.append(" -v --version   :  print version and exit\n");
        sb.append(" -V --verbose   :  alias for --loglevel=INFO\n");
        sb.append(" -a --accurate  :  accurate time measurement (does not timeout)\n");
        sb.append(" -t --timeout   :  timeout in seconds (default: 2)\n");
        sb.append(" -l --list      :  list system and config properties\n");
        sb.append(" -d --dotfile   :  create a dot-file (see manual for dot/graphviz)\n");
        sb.append(" -m --maxpaths  :  max number of open paths (default: 1000)\n");
        sb.append(" -P --paths     :  print number of paths/branches during run\n");
        sb.append(" -r --recursive :  recursively prove all files in directory\n");
        sb.append(" -s --strategy  :  simple, rete, hrete, all, main (default: main)\n");
        sb.append(" -o --order     :  match order [hash,time,random] (default: hash)\n");
        sb.append(" -p --plain     :  no ANSI colors printed \n");
        sb.append(" -c --cmp       :  comparator: see -listcmp  (default: natural)\n");
        sb.append(" -i --ignore    :  ignore fact-set, i.e. allow re-use of facts\n");
        sb.append(" --listcmp      :  list comparators and explanation\n");
        sb.append(" --single       :  match only first new fact each round\n");
        sb.append(" --seed         :  for randomized strategies (default: 0)\n");
        sb.append(" --dotfmt       :  convert dot file to format (default:eps)\n");
        sb.append(" --dotmax       :  max number of nodes in dotfile\n");
        sb.append(" --dotheader    :  font size of header in dot file (default:25)\n");
        sb.append(" --loglevel     :  DEBUG, INFO, WARNING(default), ERROR, FATAL\n");
        sb.append(" --ll           :  alias for --loglevel\n");
        sb.append(" --logfile      :  write to logfile as well as stderr\n");
        sb.append(" --lf           :  alias for --logfile\n");
        sb.append(" --hidden       :  include hidden dir/files (.somedir/.somefile)\n\n");

        System.out.print(sb.toString());
        System.exit(0);
    }

    private void printVersion(){
        System.out.printf("%s\n", Global.get("version"));
        System.exit(0);
    }
}
